$\forall$$A$:Type, ${\it eq}$:EqDecider($A$), $B$:($A$$\rightarrow$Type), $f$:$a$:$A$ fp$\rightarrow$ $B$($a$), $x$:$A$, $v$:$B$($x$).
\\[0ex]$f$ $\parallel$ $x$ : $v$ $\Rightarrow$ $x$ $\in$ dom($f$) $\Rightarrow$ $f$($x$) $=$ $v$